<?xml version="1.0" encoding="ascii"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
          "DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
  <title>spade.logic.logicTest</title>
  <link rel="stylesheet" href="epydoc.css" type="text/css" />
  <script type="text/javascript" src="epydoc.js"></script>
</head>

<body bgcolor="white" text="black" link="blue" vlink="#204080"
      alink="#204080">
<!-- ==================== NAVIGATION BAR ==================== -->
<table class="navbar" border="0" width="100%" cellpadding="0"
       bgcolor="#a0c0ff" cellspacing="0">
  <tr valign="middle">
  <!-- Home link -->
      <th>&nbsp;&nbsp;&nbsp;<a
        href="spade-module.html">Home</a>&nbsp;&nbsp;&nbsp;</th>

  <!-- Tree link -->
      <th>&nbsp;&nbsp;&nbsp;<a
        href="module-tree.html">Trees</a>&nbsp;&nbsp;&nbsp;</th>

  <!-- Index link -->
      <th>&nbsp;&nbsp;&nbsp;<a
        href="identifier-index.html">Indices</a>&nbsp;&nbsp;&nbsp;</th>

  <!-- Help link -->
      <th>&nbsp;&nbsp;&nbsp;<a
        href="help.html">Help</a>&nbsp;&nbsp;&nbsp;</th>

      <th class="navbar" width="100%"></th>
  </tr>
</table>
<table width="100%" cellpadding="0" cellspacing="0">
  <tr valign="top">
    <td width="100%">
      <span class="breadcrumbs">
        <a href="spade-module.html">Package&nbsp;spade</a> ::
        <a href="spade.logic-module.html">Module&nbsp;logic</a> ::
        Class&nbsp;logicTest
      </span>
    </td>
    <td>
      <table cellpadding="0" cellspacing="0">
        <!-- hide/show private -->
        <tr><td align="right"><span class="options">[<a href="javascript:void(0);" class="privatelink"
    onclick="toggle_private();">hide&nbsp;private</a>]</span></td></tr>
        <tr><td align="right"><span class="options"
            >[<a href="frames.html" target="_top">frames</a
            >]&nbsp;|&nbsp;<a href="spade.logic.logicTest-class.html"
            target="_top">no&nbsp;frames</a>]</span></td></tr>
      </table>
    </td>
  </tr>
</table>
<!-- ==================== CLASS DESCRIPTION ==================== -->
<h1 class="epydoc">Class logicTest</h1><p class="nomargin-top"><span class="codelink"><a href="spade.logic-pysrc.html#logicTest">source&nbsp;code</a></span></p>
<p>### PropKB &gt;&gt;&gt; kb = PropKB() &gt;&gt;&gt; kb.tell(A &amp; B) 
  &gt;&gt;&gt; kb.tell(B &gt;&gt; C) &gt;&gt;&gt; kb.ask(C) ## The result 
  {} means true, with no substitutions {} &gt;&gt;&gt; kb.ask(P) False 
  &gt;&gt;&gt; kb.retract(B) &gt;&gt;&gt; kb.ask(C) False</p>
<pre class="py-doctest">
<span class="py-prompt">&gt;&gt;&gt; </span>pl_true(P, {}) 
<span class="py-prompt">&gt;&gt;&gt; </span>pl_true(P | Q, {P: True}) 
<span class="py-output">True</span></pre>
  <p># Notice that the function pl_true cannot reason by cases: 
  &gt;&gt;&gt; pl_true(P | ~P)</p>
  <p># However, tt_true can: &gt;&gt;&gt; tt_true(P | ~P) True</p>
  <p># The following are tautologies from [Fig. 7.11]: &gt;&gt;&gt; 
  tt_true(&quot;(A &amp; B) &lt;=&gt; (B &amp; A)&quot;) True &gt;&gt;&gt; 
  tt_true(&quot;(A | B) &lt;=&gt; (B | A)&quot;) True &gt;&gt;&gt; 
  tt_true(&quot;((A &amp; B) &amp; C) &lt;=&gt; (A &amp; (B &amp; 
  C))&quot;) True &gt;&gt;&gt; tt_true(&quot;((A | B) | C) &lt;=&gt; (A | 
  (B | C))&quot;) True &gt;&gt;&gt; tt_true(&quot;~~A &lt;=&gt; A&quot;) 
  True &gt;&gt;&gt; tt_true(&quot;(A &gt;&gt; B) &lt;=&gt; (~B &gt;&gt; 
  ~A)&quot;) True &gt;&gt;&gt; tt_true(&quot;(A &gt;&gt; B) &lt;=&gt; (~A |
  B)&quot;) True &gt;&gt;&gt; tt_true(&quot;(A &lt;=&gt; B) &lt;=&gt; ((A 
  &gt;&gt; B) &amp; (B &gt;&gt; A))&quot;) True &gt;&gt;&gt; 
  tt_true(&quot;~(A &amp; B) &lt;=&gt; (~A | ~B)&quot;) True &gt;&gt;&gt; 
  tt_true(&quot;~(A | B) &lt;=&gt; (~A &amp; ~B)&quot;) True &gt;&gt;&gt; 
  tt_true(&quot;(A &amp; (B | C)) &lt;=&gt; ((A &amp; B) | (A &amp; 
  C))&quot;) True &gt;&gt;&gt; tt_true(&quot;(A | (B &amp; C)) &lt;=&gt; 
  ((A | B) &amp; (A | C))&quot;) True</p>
  <p># The following are not tautologies: &gt;&gt;&gt; tt_true(A &amp; ~A) 
  False &gt;&gt;&gt; tt_true(A &amp; B) False</p>
  <p>### [Fig. 7.13] &gt;&gt;&gt; alpha = expr(&quot;~P12&quot;) 
  &gt;&gt;&gt; to_cnf(Fig[7,13] &amp; ~alpha) ((~P12 | B11) &amp; (~P21 | 
  B11) &amp; (P12 | P21 | ~B11) &amp; ~B11 &amp; P12) &gt;&gt;&gt; 
  tt_entails(Fig[7,13], alpha) True &gt;&gt;&gt; 
  pl_resolution(PropKB(Fig[7,13]), alpha) True</p>
  <p>### [Fig. 7.15] &gt;&gt;&gt; pl_fc_entails(Fig[7,15], 
  expr('SomethingSilly')) False</p>
  <p>### Unification: &gt;&gt;&gt; unify(x, x, {}) {} &gt;&gt;&gt; unify(x,
  3, {}) {x: 3}</p>
<pre class="py-doctest">
<span class="py-prompt">&gt;&gt;&gt; </span>to_cnf((P&amp;Q) | (~P &amp; ~Q)) 
<span class="py-output">((~P | P) &amp; (~Q | P) &amp; (~P | Q) &amp; (~Q | Q))</span></pre>

<!-- ==================== NAVIGATION BAR ==================== -->
<table class="navbar" border="0" width="100%" cellpadding="0"
       bgcolor="#a0c0ff" cellspacing="0">
  <tr valign="middle">
  <!-- Home link -->
      <th>&nbsp;&nbsp;&nbsp;<a
        href="spade-module.html">Home</a>&nbsp;&nbsp;&nbsp;</th>

  <!-- Tree link -->
      <th>&nbsp;&nbsp;&nbsp;<a
        href="module-tree.html">Trees</a>&nbsp;&nbsp;&nbsp;</th>

  <!-- Index link -->
      <th>&nbsp;&nbsp;&nbsp;<a
        href="identifier-index.html">Indices</a>&nbsp;&nbsp;&nbsp;</th>

  <!-- Help link -->
      <th>&nbsp;&nbsp;&nbsp;<a
        href="help.html">Help</a>&nbsp;&nbsp;&nbsp;</th>

      <th class="navbar" width="100%"></th>
  </tr>
</table>
<table border="0" cellpadding="0" cellspacing="0" width="100%%">
  <tr>
    <td align="left" class="footer">
    Generated by Epydoc 3.0.1 on Wed May 26 16:26:24 2010
    </td>
    <td align="right" class="footer">
      <a target="mainFrame" href="http://epydoc.sourceforge.net"
        >http://epydoc.sourceforge.net</a>
    </td>
  </tr>
</table>

<script type="text/javascript">
  <!--
  // Private objects are initially displayed (because if
  // javascript is turned off then we want them to be
  // visible); but by default, we want to hide them.  So hide
  // them unless we have a cookie that says to show them.
  checkCookie();
  // -->
</script>
</body>
</html>
